Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(rev,nil)  → nil
2:    app(rev,app(app(cons,x),l))  → app(app(cons,app(app(rev1,x),l)),app(app(rev2,x),l))
3:    app(app(rev1,0),nil)  → 0
4:    app(app(rev1,app(s,x)),nil)  → app(s,x)
5:    app(app(rev1,x),app(app(cons,y),l))  → app(app(rev1,y),l)
6:    app(app(rev2,x),nil)  → nil
7:    app(app(rev2,x),app(app(cons,y),l))  → app(rev,app(app(cons,x),app(app(rev2,y),l)))
There are 13 dependency pairs:
8:    APP(rev,app(app(cons,x),l))  → APP(app(cons,app(app(rev1,x),l)),app(app(rev2,x),l))
9:    APP(rev,app(app(cons,x),l))  → APP(cons,app(app(rev1,x),l))
10:    APP(rev,app(app(cons,x),l))  → APP(app(rev1,x),l)
11:    APP(rev,app(app(cons,x),l))  → APP(rev1,x)
12:    APP(rev,app(app(cons,x),l))  → APP(app(rev2,x),l)
13:    APP(rev,app(app(cons,x),l))  → APP(rev2,x)
14:    APP(app(rev1,x),app(app(cons,y),l))  → APP(app(rev1,y),l)
15:    APP(app(rev1,x),app(app(cons,y),l))  → APP(rev1,y)
16:    APP(app(rev2,x),app(app(cons,y),l))  → APP(rev,app(app(cons,x),app(app(rev2,y),l)))
17:    APP(app(rev2,x),app(app(cons,y),l))  → APP(app(cons,x),app(app(rev2,y),l))
18:    APP(app(rev2,x),app(app(cons,y),l))  → APP(cons,x)
19:    APP(app(rev2,x),app(app(cons,y),l))  → APP(app(rev2,y),l)
20:    APP(app(rev2,x),app(app(cons,y),l))  → APP(rev2,y)
The approximated dependency graph contains one SCC: {8,10,12,14,16,17,19}.
Tyrolean Termination Tool  (0.24 seconds)   ---  May 3, 2006